_ALICE_ =
    {privkey=<RSAKeyValue><Modulus>kUWXmVPrxaQBAE+hxwzlzo/+hOTL60RIa2O+Ud0vnUUTB0OO+znVakY2dXnW/hqMa7cx49GCUFUx7iTv4cFYHPtAzFecyrbIzwLBdhbcATj2qpRVsrSoBtVRxEAqiktil5IhtCk7usy85HYDxNbVw/HWHvQRTd6cuYnKb4KNU1E=</Modulus><Exponent>AQAB</Exponent><P>xq4lK+sSdwEB1fCcyW5wQKfx74TWx+uxXjHunyXDKZhgkNiZ685VWr1kuiCfil2jOp8Hc/9WnlxcdH1nGvQXiQ==</P><Q>uy7hr+TXGQDNXyrje4MOIR9ZAlN1Oz5henc5IKBn+ddqlUQKH9rIqI/PQgBvT44bnnybBr2DiStafB9Hbs0jiQ==</Q><DP>xMnelZabznWX7OELWtThqJjwoM5Rsul34BXTBZ1wpjWAiFeSdacEkgD/0P/ZJkLDF6BG0JU7pVVUWimPw3m8CQ==</DP><DQ>hGb8AuQ29huoKXn34QTpuKoo1slb8iUE5JBym057XbFvVdgD5VZnezwGGaSfF8HobWmsas8gvKUq4wNpDsoSKQ==</DQ><InverseQ>nRitOmPpVe1vKg3Qq1+2SpCOlKxbfEED22CkRJxLVj8ElX0foB38RNJhHxnPvCAEvGdXVRLdeA4N5/nqU/pNyA==</InverseQ><D>N06ue+KWdeWNuAeZSQYhC/aIaSIOfOC/TZto3xP9x7t/lhlje0Q2e0KGA03Cy3ViFrRlWx3tphX5b3hCl8mbeMJLeOk8RFAWHVe3IpKr3Op+D8P2SD20/UopC4RaMlwsNSW++7a2ldifHCobZTwIAK68eR1cSL3gUt/sqnZOhcE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>kUWXmVPrxaQBAE+hxwzlzo/+hOTL60RIa2O+Ud0vnUUTB0OO+znVakY2dXnW/hqMa7cx49GCUFUx7iTv4cFYHPtAzFecyrbIzwLBdhbcATj2qpRVsrSoBtVRxEAqiktil5IhtCk7usy85HYDxNbVw/HWHvQRTd6cuYnKb4KNU1E=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6301}

and _BOB_ = 
    {privkey=<RSAKeyValue><Modulus>w82NXJIdeCJnm9vNadVHErCaRkoCfU8pap6LDw6N27yHRTTcQcTYZD27D20Nsji21cljjhhpefocP3sa6zeI+VjgtWBB16axdh3eROyyC/1vpS8Q2TIraBrp6Ew8ld51/p35tu5HZhuzN2gltgSTrzsMOvNGfz4HIVUt+DjuDDk=</Modulus><Exponent>AQAB</Exponent><P>8odIOrLxHyb6lbh5qXd+BBMMOo0BDbH+W/B39y3+2YmSEb3uHhpUA+lrf3bMf0BXLRw695nUtWpC6b+sgo3pZQ==</P><Q>zq3XI8r6y2lwHTddCmczOWYL8oCz+z8t9Jf9/LPg+IN8HnYFxRy5ICLNzx0dgG3WaC4wjpk/royFQ3WTQqVURQ==</Q><DP>0jumxwtarPBzA9oXzGlCmXGRhie4pBCJN1VqCKCcbCIutqZ3hSy5a3KptqJafmxdpUL1crCsjF4ChvGaLsmpaQ==</DP><DQ>qot6jveMsdNEh2dK6C22cDPLwgT//1/oDQBqvl60Un01K3GaW0fTXzg4+iH9WR/Jn9gVi2Xbza34vWzE4mbIvQ==</DQ><InverseQ>0ZcWjOdE2Z3F9fdluvKeerIezF/3gzTmdHd9CYwPK/sIuEFP3tF0jzzJxGKFybxaGq0RYcnkkw74LwXSVOsJaw==</InverseQ><D>LkwECMdjwGwiI3AtecC8NWcck1IclJSLLnKeXskKMdK6CVseWU65+7m86UDX5DQUxyf/KjILfpPs6fWpv8Q51pE+ORHhyXOKPLDj/5vgHa0WFvFK3NoCsvB/ahIKINF+XpsWD7AmBWNJUPuqxZrCyYzv7qPT24gEJZCV9scmfIE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>w82NXJIdeCJnm9vNadVHErCaRkoCfU8pap6LDw6N27yHRTTcQcTYZD27D20Nsji21cljjhhpefocP3sa6zeI+VjgtWBB16axdh3eROyyC/1vpS8Q2TIraBrp6Ew8ld51/p35tu5HZhuzN2gltgSTrzsMOvNGfz4HIVUt+DjuDDk=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6302}

and _CHUCK_ =
    {privkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent><P>/rEL5XxETzzYLznPHnFOOHCH+q/61GyB5XY/rWO5kEQygx+wOJNpwZ4F453/v8dTg5epedz4DDlAeJ23LUNjiQ==</P><Q>57oTxICOcOQ6Y0Poaw6vyBwcCHViQMZBBuJH34rUeAmkaG/EG44M51dZ1Y7ictYVI8uoU7d+/59KiGeRhcSv/w==</Q><DP>idQyBeyr4t2geF4mcekLVYvAaq+VZCOcYBsP9rtDDol5dHBPoy5TSw5DTZyRbK1nyozmkCY+rg7FjwB6wqn3UQ==</DP><DQ>ISX2M/Lr7WxIifCp676jGK4kuHUKRBfYL4LpIyo58J34fdQXKpXsdJ+DQ1B4RlMnnQJCJw+lxC1mPRMLtyYGww==</DQ><InverseQ>JChw7RjvCI7B9w1XBEvEoO+87RX4n/uuAnHFa2deRLLht7HN9XAibConnUcSWuHl1CJnCmhsqniR7ds90oigeQ==</InverseQ><D>kC90Rx2+7FEFtEkg9xbEXoVWSUbJk2OfX6z7I5ZYHyRq0TaC0LWXtyqTx+171axB1Oxs8c1+czmAucOM0tKsgeLK+v+fAv9yioU2eYSu+VfSwfZoUgtxVyqXuDOmujE6QU8grtMej1qR4MMytrafBGlWcYEXFo9vmWIsVmIROkE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6303}

and _PRESS_ =
    {privkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent><P>/rEL5XxETzzYLznPHnFOOHCH+q/61GyB5XY/rWO5kEQygx+wOJNpwZ4F453/v8dTg5epedz4DDlAeJ23LUNjiQ==</P><Q>57oTxICOcOQ6Y0Poaw6vyBwcCHViQMZBBuJH34rUeAmkaG/EG44M51dZ1Y7ictYVI8uoU7d+/59KiGeRhcSv/w==</Q><DP>idQyBeyr4t2geF4mcekLVYvAaq+VZCOcYBsP9rtDDol5dHBPoy5TSw5DTZyRbK1nyozmkCY+rg7FjwB6wqn3UQ==</DP><DQ>ISX2M/Lr7WxIifCp676jGK4kuHUKRBfYL4LpIyo58J34fdQXKpXsdJ+DQ1B4RlMnnQJCJw+lxC1mPRMLtyYGww==</DQ><InverseQ>JChw7RjvCI7B9w1XBEvEoO+87RX4n/uuAnHFa2deRLLht7HN9XAibConnUcSWuHl1CJnCmhsqniR7ds90oigeQ==</InverseQ><D>kC90Rx2+7FEFtEkg9xbEXoVWSUbJk2OfX6z7I5ZYHyRq0TaC0LWXtyqTx+171axB1Oxs8c1+czmAucOM0tKsgeLK+v+fAv9yioU2eYSu+VfSwfZoUgtxVyqXuDOmujE6QU8grtMej1qR4MMytrafBGlWcYEXFo9vmWIsVmIROkE=</D></RSAKeyValue>;
     pubkey=<RSAKeyValue><Modulus>5oriCVszTYWL3NEXAriyAuie+49LfKwZgNBs1EOgf+QU0ioleDIEufy4fVJ9+82uacRNb50rTMWwhlW7iWDBNC+y4sWbNNLmplg8tBWOq3nd+KMAPecTcvo6t6OCfX5TgGNQ4mbzldiCOTTWZ5cBzyLSSVS3XS4C0bd7TokOzHc=</Modulus><Exponent>AQAB</Exponent></RSAKeyValue>;
     port=6304}

and Init of int
and IsTheNextBigStar of prin
and $let neq x y (env:substitution) : term =
      let _ = println "neq starting ...." in
       match (lookupName env x Principal), (lookupName env y Principal) with
	     | Some (Const (PrincipalConstant px)), Some (Const (PrincipalConstant py)) ->  
		   let _ = println (strcat "px = " px) in
		   let _ = println (strcat "py = " py) in
		   App (if (px = py) then  FalseInfon else EmptyInfon) []
		 | z -> let _ = println "not matching ...." in 
		        let _ = println (string_of_any_for_coq env) in
				App FalseInfon []
    $